Termination w.r.t. Q proof of /tmp/tmp0BF

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(true, x, y, z) → g(gt(x, y), x, y, z)
g(true, x, y, z) → f(gt(x, z), x, s(y), z)
g(true, x, y, z) → f(gt(x, z), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

Q is empty.

↳ QTRS

  ↳ AAECC Innermost

Q restricted rewrite system:
The TRS R consists of the following rules:

f(true, x, y, z) → g(gt(x, y), x, y, z)
g(true, x, y, z) → f(gt(x, z), x, s(y), z)
g(true, x, y, z) → f(gt(x, z), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

Q is empty.

We have applied [19,8] to switch to innermost. The TRS R 1 is

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The TRS R 2 is

f(true, x, y, z) → g(gt(x, y), x, y, z)
g(true, x, y, z) → f(gt(x, z), x, s(y), z)
g(true, x, y, z) → f(gt(x, z), x, y, s(z))

The signature Sigma is {f, g}

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(true, x, y, z) → g(gt(x, y), x, y, z)
g(true, x, y, z) → f(gt(x, z), x, s(y), z)
g(true, x, y, z) → f(gt(x, z), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
g(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

G(true, x, y, z) → F(gt(x, z), x, y, s(z))
F(true, x, y, z) → GT(x, y)
GT(s(u), s(v)) → GT(u, v)
G(true, x, y, z) → F(gt(x, z), x, s(y), z)
G(true, x, y, z) → GT(x, z)
F(true, x, y, z) → G(gt(x, y), x, y, z)

The TRS R consists of the following rules:

f(true, x, y, z) → g(gt(x, y), x, y, z)
g(true, x, y, z) → f(gt(x, z), x, s(y), z)
g(true, x, y, z) → f(gt(x, z), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
g(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

G(true, x, y, z) → F(gt(x, z), x, y, s(z))
F(true, x, y, z) → GT(x, y)
GT(s(u), s(v)) → GT(u, v)
G(true, x, y, z) → F(gt(x, z), x, s(y), z)
G(true, x, y, z) → GT(x, z)
F(true, x, y, z) → G(gt(x, y), x, y, z)

The TRS R consists of the following rules:

f(true, x, y, z) → g(gt(x, y), x, y, z)
g(true, x, y, z) → f(gt(x, z), x, s(y), z)
g(true, x, y, z) → f(gt(x, z), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
g(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(u), s(v)) → GT(u, v)

The TRS R consists of the following rules:

f(true, x, y, z) → g(gt(x, y), x, y, z)
g(true, x, y, z) → f(gt(x, z), x, s(y), z)
g(true, x, y, z) → f(gt(x, z), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
g(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(u), s(v)) → GT(u, v)

R is empty.
The set Q consists of the following terms:

f(true, x0, x1, x2)
g(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

f(true, x0, x1, x2)
g(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT(s(u), s(v)) → GT(u, v)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

GT(s(u), s(v)) → GT(u, v)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

G(true, x, y, z) → F(gt(x, z), x, y, s(z))
G(true, x, y, z) → F(gt(x, z), x, s(y), z)
F(true, x, y, z) → G(gt(x, y), x, y, z)

The TRS R consists of the following rules:

f(true, x, y, z) → g(gt(x, y), x, y, z)
g(true, x, y, z) → f(gt(x, z), x, s(y), z)
g(true, x, y, z) → f(gt(x, z), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
g(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

G(true, x, y, z) → F(gt(x, z), x, y, s(z))
G(true, x, y, z) → F(gt(x, z), x, s(y), z)
F(true, x, y, z) → G(gt(x, y), x, y, z)

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

f(true, x0, x1, x2)
g(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

f(true, x0, x1, x2)
g(true, x0, x1, x2)

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ NonInfProof

Q DP problem:
The TRS P consists of the following rules:

G(true, x, y, z) → F(gt(x, z), x, y, s(z))
G(true, x, y, z) → F(gt(x, z), x, s(y), z)
F(true, x, y, z) → G(gt(x, y), x, y, z)

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The DP Problem is simplified using the Induction Calculus [18] with the following steps:
Note that final constraints are written in bold face.

For Pair G(true, x, y, z) → F(gt(x, z), x, y, s(z)) the following chains were created:

We consider the chain F(true, x, y, z) → G(gt(x, y), x, y, z), G(true, x, y, z) → F(gt(x, z), x, y, s(z)) which results in the following constraint:
(1)    (G(gt(x6, x7), x6, x7, x8)=G(true, x9, x10, x11) ⇒ G(true, x9, x10, x11)≥F(gt(x9, x11), x9, x10, s(x11)))

We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2)    (gt(x6, x7)=true ⇒ G(true, x6, x7, x8)≥F(gt(x6, x8), x6, x7, s(x8)))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on gt(x6, x7)=true which results in the following new constraints:
(3)    (true=true ⇒ G(true, s(x40), 0, x8)≥F(gt(s(x40), x8), s(x40), 0, s(x8)))

(4)    (gt(x41, x42)=true∧(∀x43:gt(x41, x42)=true ⇒ G(true, x41, x42, x43)≥F(gt(x41, x43), x41, x42, s(x43))) ⇒ G(true, s(x41), s(x42), x8)≥F(gt(s(x41), x8), s(x41), s(x42), s(x8)))

We simplified constraint (3) using rules (I), (II) which results in the following new constraint:
(5)    (G(true, s(x40), 0, x8)≥F(gt(s(x40), x8), s(x40), 0, s(x8)))

We simplified constraint (4) using rule (VI) where we applied the induction hypothesis (∀x43:gt(x41, x42)=true ⇒ G(true, x41, x42, x43)≥F(gt(x41, x43), x41, x42, s(x43))) with σ = [x43 / x8] which results in the following new constraint:
(6)    (G(true, x41, x42, x8)≥F(gt(x41, x8), x41, x42, s(x8)) ⇒ G(true, s(x41), s(x42), x8)≥F(gt(s(x41), x8), s(x41), s(x42), s(x8)))

For Pair G(true, x, y, z) → F(gt(x, z), x, s(y), z) the following chains were created:

We consider the chain F(true, x, y, z) → G(gt(x, y), x, y, z), G(true, x, y, z) → F(gt(x, z), x, s(y), z) which results in the following constraint:
(7)    (G(gt(x18, x19), x18, x19, x20)=G(true, x21, x22, x23) ⇒ G(true, x21, x22, x23)≥F(gt(x21, x23), x21, s(x22), x23))

We simplified constraint (7) using rules (I), (II), (III) which results in the following new constraint:
(8)    (gt(x18, x19)=true ⇒ G(true, x18, x19, x20)≥F(gt(x18, x20), x18, s(x19), x20))

We simplified constraint (8) using rule (V) (with possible (I) afterwards) using induction on gt(x18, x19)=true which results in the following new constraints:
(9)    (true=true ⇒ G(true, s(x45), 0, x20)≥F(gt(s(x45), x20), s(x45), s(0), x20))

(10)    (gt(x46, x47)=true∧(∀x48:gt(x46, x47)=true ⇒ G(true, x46, x47, x48)≥F(gt(x46, x48), x46, s(x47), x48)) ⇒ G(true, s(x46), s(x47), x20)≥F(gt(s(x46), x20), s(x46), s(s(x47)), x20))

We simplified constraint (9) using rules (I), (II) which results in the following new constraint:
(11)    (G(true, s(x45), 0, x20)≥F(gt(s(x45), x20), s(x45), s(0), x20))

We simplified constraint (10) using rule (VI) where we applied the induction hypothesis (∀x48:gt(x46, x47)=true ⇒ G(true, x46, x47, x48)≥F(gt(x46, x48), x46, s(x47), x48)) with σ = [x48 / x20] which results in the following new constraint:
(12)    (G(true, x46, x47, x20)≥F(gt(x46, x20), x46, s(x47), x20) ⇒ G(true, s(x46), s(x47), x20)≥F(gt(s(x46), x20), s(x46), s(s(x47)), x20))

For Pair F(true, x, y, z) → G(gt(x, y), x, y, z) the following chains were created:

We consider the chain G(true, x, y, z) → F(gt(x, z), x, y, s(z)), F(true, x, y, z) → G(gt(x, y), x, y, z) which results in the following constraint:
(13)    (F(gt(x24, x26), x24, x25, s(x26))=F(true, x27, x28, x29) ⇒ F(true, x27, x28, x29)≥G(gt(x27, x28), x27, x28, x29))

We simplified constraint (13) using rules (I), (II), (III) which results in the following new constraint:
(14)    (gt(x24, x26)=true ⇒ F(true, x24, x25, s(x26))≥G(gt(x24, x25), x24, x25, s(x26)))

We simplified constraint (14) using rule (V) (with possible (I) afterwards) using induction on gt(x24, x26)=true which results in the following new constraints:
(15)    (true=true ⇒ F(true, s(x50), x25, s(0))≥G(gt(s(x50), x25), s(x50), x25, s(0)))

(16)    (gt(x51, x52)=true∧(∀x53:gt(x51, x52)=true ⇒ F(true, x51, x53, s(x52))≥G(gt(x51, x53), x51, x53, s(x52))) ⇒ F(true, s(x51), x25, s(s(x52)))≥G(gt(s(x51), x25), s(x51), x25, s(s(x52))))

We simplified constraint (15) using rules (I), (II) which results in the following new constraint:
(17)    (F(true, s(x50), x25, s(0))≥G(gt(s(x50), x25), s(x50), x25, s(0)))

We simplified constraint (16) using rule (VI) where we applied the induction hypothesis (∀x53:gt(x51, x52)=true ⇒ F(true, x51, x53, s(x52))≥G(gt(x51, x53), x51, x53, s(x52))) with σ = [x53 / x25] which results in the following new constraint:
(18)    (F(true, x51, x25, s(x52))≥G(gt(x51, x25), x51, x25, s(x52)) ⇒ F(true, s(x51), x25, s(s(x52)))≥G(gt(s(x51), x25), s(x51), x25, s(s(x52))))
We consider the chain G(true, x, y, z) → F(gt(x, z), x, s(y), z), F(true, x, y, z) → G(gt(x, y), x, y, z) which results in the following constraint:
(19)    (F(gt(x30, x32), x30, s(x31), x32)=F(true, x33, x34, x35) ⇒ F(true, x33, x34, x35)≥G(gt(x33, x34), x33, x34, x35))

We simplified constraint (19) using rules (I), (II), (III) which results in the following new constraint:
(20)    (gt(x30, x32)=true ⇒ F(true, x30, s(x31), x32)≥G(gt(x30, s(x31)), x30, s(x31), x32))

We simplified constraint (20) using rule (V) (with possible (I) afterwards) using induction on gt(x30, x32)=true which results in the following new constraints:
(21)    (true=true ⇒ F(true, s(x55), s(x31), 0)≥G(gt(s(x55), s(x31)), s(x55), s(x31), 0))

(22)    (gt(x56, x57)=true∧(∀x58:gt(x56, x57)=true ⇒ F(true, x56, s(x58), x57)≥G(gt(x56, s(x58)), x56, s(x58), x57)) ⇒ F(true, s(x56), s(x31), s(x57))≥G(gt(s(x56), s(x31)), s(x56), s(x31), s(x57)))

We simplified constraint (21) using rules (I), (II) which results in the following new constraint:
(23)    (F(true, s(x55), s(x31), 0)≥G(gt(s(x55), s(x31)), s(x55), s(x31), 0))

We simplified constraint (22) using rule (VI) where we applied the induction hypothesis (∀x58:gt(x56, x57)=true ⇒ F(true, x56, s(x58), x57)≥G(gt(x56, s(x58)), x56, s(x58), x57)) with σ = [x58 / x31] which results in the following new constraint:
(24)    (F(true, x56, s(x31), x57)≥G(gt(x56, s(x31)), x56, s(x31), x57) ⇒ F(true, s(x56), s(x31), s(x57))≥G(gt(s(x56), s(x31)), s(x56), s(x31), s(x57)))

To summarize, we get the following constraints P_≥ for the following pairs.

G(true, x, y, z) → F(gt(x, z), x, y, s(z))
- (G(true, s(x40), 0, x8)≥F(gt(s(x40), x8), s(x40), 0, s(x8)))
- (G(true, x41, x42, x8)≥F(gt(x41, x8), x41, x42, s(x8)) ⇒ G(true, s(x41), s(x42), x8)≥F(gt(s(x41), x8), s(x41), s(x42), s(x8)))
G(true, x, y, z) → F(gt(x, z), x, s(y), z)
- (G(true, s(x45), 0, x20)≥F(gt(s(x45), x20), s(x45), s(0), x20))
- (G(true, x46, x47, x20)≥F(gt(x46, x20), x46, s(x47), x20) ⇒ G(true, s(x46), s(x47), x20)≥F(gt(s(x46), x20), s(x46), s(s(x47)), x20))
F(true, x, y, z) → G(gt(x, y), x, y, z)
- (F(true, s(x50), x25, s(0))≥G(gt(s(x50), x25), s(x50), x25, s(0)))
- (F(true, x51, x25, s(x52))≥G(gt(x51, x25), x51, x25, s(x52)) ⇒ F(true, s(x51), x25, s(s(x52)))≥G(gt(s(x51), x25), s(x51), x25, s(s(x52))))
- (F(true, s(x55), s(x31), 0)≥G(gt(s(x55), s(x31)), s(x55), s(x31), 0))
- (F(true, x56, s(x31), x57)≥G(gt(x56, s(x31)), x56, s(x31), x57) ⇒ F(true, s(x56), s(x31), s(x57))≥G(gt(s(x56), s(x31)), s(x56), s(x31), s(x57)))

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [18]:

POL(0) = 0
POL(F(x₁, x₂, x₃, x₄)) = -1 - x₁ + x₂ - x₄
POL(G(x₁, x₂, x₃, x₄)) = -1 - x₁ + x₂ - x₄
POL(c) = -1
POL(false) = 0
POL(gt(x₁, x₂)) = 0
POL(s(x₁)) = 1 + x₁
POL(true) = 0

The following pairs are in P_>:

G(true, x, y, z) → F(gt(x, z), x, y, s(z))

The following pairs are in P_bound:

F(true, x, y, z) → G(gt(x, y), x, y, z)

The following rules are usable:

gt(u, v) → gt(s(u), s(v))
false → gt(0, v)
true → gt(s(u), 0)

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ NonInfProof

                          ↳ AND

                            ↳ QDP

                              ↳ NonInfProof

                            ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

G(true, x, y, z) → F(gt(x, z), x, s(y), z)
F(true, x, y, z) → G(gt(x, y), x, y, z)

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We consider the chain F(true, x, y, z) → G(gt(x, y), x, y, z), G(true, x, y, z) → F(gt(x, z), x, s(y), z) which results in the following constraint:
(1)    (G(gt(x18, x19), x18, x19, x20)=G(true, x21, x22, x23) ⇒ G(true, x21, x22, x23)≥F(gt(x21, x23), x21, s(x22), x23))

We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2)    (gt(x18, x19)=true ⇒ G(true, x18, x19, x20)≥F(gt(x18, x20), x18, s(x19), x20))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on gt(x18, x19)=true which results in the following new constraints:
(3)    (true=true ⇒ G(true, s(x45), 0, x20)≥F(gt(s(x45), x20), s(x45), s(0), x20))

(4)    (gt(x46, x47)=true∧(∀x48:gt(x46, x47)=true ⇒ G(true, x46, x47, x48)≥F(gt(x46, x48), x46, s(x47), x48)) ⇒ G(true, s(x46), s(x47), x20)≥F(gt(s(x46), x20), s(x46), s(s(x47)), x20))

We simplified constraint (3) using rules (I), (II) which results in the following new constraint:
(5)    (G(true, s(x45), 0, x20)≥F(gt(s(x45), x20), s(x45), s(0), x20))

We simplified constraint (4) using rule (VI) where we applied the induction hypothesis (∀x48:gt(x46, x47)=true ⇒ G(true, x46, x47, x48)≥F(gt(x46, x48), x46, s(x47), x48)) with σ = [x48 / x20] which results in the following new constraint:
(6)    (G(true, x46, x47, x20)≥F(gt(x46, x20), x46, s(x47), x20) ⇒ G(true, s(x46), s(x47), x20)≥F(gt(s(x46), x20), s(x46), s(s(x47)), x20))

For Pair F(true, x, y, z) → G(gt(x, y), x, y, z) the following chains were created:

We consider the chain G(true, x, y, z) → F(gt(x, z), x, s(y), z), F(true, x, y, z) → G(gt(x, y), x, y, z) which results in the following constraint:
(7)    (F(gt(x30, x32), x30, s(x31), x32)=F(true, x33, x34, x35) ⇒ F(true, x33, x34, x35)≥G(gt(x33, x34), x33, x34, x35))

We simplified constraint (7) using rules (I), (II), (III) which results in the following new constraint:
(8)    (gt(x30, x32)=true ⇒ F(true, x30, s(x31), x32)≥G(gt(x30, s(x31)), x30, s(x31), x32))

We simplified constraint (8) using rule (V) (with possible (I) afterwards) using induction on gt(x30, x32)=true which results in the following new constraints:
(9)    (true=true ⇒ F(true, s(x55), s(x31), 0)≥G(gt(s(x55), s(x31)), s(x55), s(x31), 0))

(10)    (gt(x56, x57)=true∧(∀x58:gt(x56, x57)=true ⇒ F(true, x56, s(x58), x57)≥G(gt(x56, s(x58)), x56, s(x58), x57)) ⇒ F(true, s(x56), s(x31), s(x57))≥G(gt(s(x56), s(x31)), s(x56), s(x31), s(x57)))

We simplified constraint (9) using rules (I), (II) which results in the following new constraint:
(11)    (F(true, s(x55), s(x31), 0)≥G(gt(s(x55), s(x31)), s(x55), s(x31), 0))

We simplified constraint (10) using rule (VI) where we applied the induction hypothesis (∀x58:gt(x56, x57)=true ⇒ F(true, x56, s(x58), x57)≥G(gt(x56, s(x58)), x56, s(x58), x57)) with σ = [x58 / x31] which results in the following new constraint:
(12)    (F(true, x56, s(x31), x57)≥G(gt(x56, s(x31)), x56, s(x31), x57) ⇒ F(true, s(x56), s(x31), s(x57))≥G(gt(s(x56), s(x31)), s(x56), s(x31), s(x57)))

To summarize, we get the following constraints P_≥ for the following pairs.

G(true, x, y, z) → F(gt(x, z), x, s(y), z)
- (G(true, s(x45), 0, x20)≥F(gt(s(x45), x20), s(x45), s(0), x20))
- (G(true, x46, x47, x20)≥F(gt(x46, x20), x46, s(x47), x20) ⇒ G(true, s(x46), s(x47), x20)≥F(gt(s(x46), x20), s(x46), s(s(x47)), x20))
F(true, x, y, z) → G(gt(x, y), x, y, z)
- (F(true, s(x55), s(x31), 0)≥G(gt(s(x55), s(x31)), s(x55), s(x31), 0))
- (F(true, x56, s(x31), x57)≥G(gt(x56, s(x31)), x56, s(x31), x57) ⇒ F(true, s(x56), s(x31), s(x57))≥G(gt(s(x56), s(x31)), s(x56), s(x31), s(x57)))

POL(0) = 0
POL(F(x₁, x₂, x₃, x₄)) = -x₁ + x₂ - x₃ + x₄
POL(G(x₁, x₂, x₃, x₄)) = -x₁ + x₂ - x₃ + x₄
POL(c) = -1
POL(false) = 0
POL(gt(x₁, x₂)) = 0
POL(s(x₁)) = 1 + x₁
POL(true) = 0

The following pairs are in P_>:

G(true, x, y, z) → F(gt(x, z), x, s(y), z)

The following pairs are in P_bound:

G(true, x, y, z) → F(gt(x, z), x, s(y), z)

The following rules are usable:

gt(u, v) → gt(s(u), s(v))
false → gt(0, v)
true → gt(s(u), 0)

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ NonInfProof

                          ↳ AND

                            ↳ QDP

                              ↳ NonInfProof

                                ↳ QDP

                                  ↳ DependencyGraphProof

                            ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(true, x, y, z) → G(gt(x, y), x, y, z)

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ QTRS

  ↳ AAECC Innermost

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ NonInfProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

G(true, x, y, z) → F(gt(x, z), x, y, s(z))
G(true, x, y, z) → F(gt(x, z), x, s(y), z)

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)

The set Q consists of the following terms:

gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.